Nuprl Lemma : alle-at-not-first
0,22
postcript
pdf
es
:ES,
i
:Id,
P
:({
e
:E| loc(
e
) =
i
}
Prop).
e
@
i
.
P
(
e
)
e
@
i
.
first(
e
)
P
(pred(
e
))
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
pred(
e
)
,
E
,
loc(
e
)
,
Id
,
Prop
,
first(
e
)
,
b
,
A
,
x
(
s
)
,
e
@
i
.
P
(
e
)
,
ES
,
x
.
t
(
x
)
,
False
Lemmas
alle-at
wf
,
event
system
wf
,
not
wf
,
assert
wf
,
es-first
wf
,
Id
wf
,
es-loc
wf
,
es-E
wf
,
es-pred
wf
,
es-loc-pred
origin
es:ES, i:Id, P:({e:E| loc(e) = i }
Prop). e@i. P(e) 
e@i. 
first(e) P(pred(e)) es:ES, i:Id, P:({e:E| loc(e) = i }Prop). e@i. P(e) e@i. first(e) P(pred(e)) 
T Qx:A. B(x)
bAe@i. P(e)
x. t(x)